ecl(${\it ds}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$rec($X$.$k$:Knd$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow\mathbb{B}$)+$X$$\times$$X$+$X$$\times$$X$+$X$$\times$$X$+$X$+$X$$\times\mathbb{N}$+$X$$\times\mathbb{N}$+$X$$\times$($\mathbb{N}$ List))